r:CRng, a:Ideal(r){i}, d:detach_fun(|r|;a), u, v:|r|.
(u = v  Carrier(r/d))  ((d(u +r (-r(v))))) 

latex

Up	rings 1
Definitions of Statement	Rng, CRng, Ideal(r){i}, Carrier(r/d)
Definitions	, t  T, P  Q, P  Q, P & Q, x f y, P  Q, x:A. B(x), True, T, Carrier(r/d), Rng, detach_fun(T;A), Ideal(r){i}, CRng, SqStable(P), S  T
Lemmas	crng wf, ideal wf, detach fun wf, rng car wf, rng minus wf, rng plus wf, assert wf, quot ring car qinc, quot ring car wf, decidable assert, sq stable from decidable